\documentclass{beamer}

\usepackage[portuguese]{babel}
\usepackage[latin1]{inputenc}
\usepackage{default}
\usepackage{array}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{xcolor}

\usetheme{Boadilla}

\newcommand{\rotimes}{\textcolor{red}{\blacklozenge}}
\newcommand{\gotimes}{\textcolor{green}{\blacklozenge}}

\title{Modela\c{c}\~ao de Esta\c{c}\~oes de Comboios}
\author{Jo\~ao Paz \and Pedro Ara\'ujo}
\date{\today}

\begin{document}

\frame{\titlepage}

\section{Problema Proposto}

\frame{
\frametitle{Objectivos}
Os objectivos para esta fase:
\begin{itemize}
 \item Passar o modelo Alloy para Java com anota\c{c}\~ao JML
 \item Utilizar JUnit para testes
 \item Testar anota\c{c}\~ao JML com JML-Junit
\end{itemize}

}

\frame{
\frametitle{Alloy para Java}
\begin{center}
% use packages: array
\begin{tabular}{ll}
\includegraphics[scale=0.2]{meta-modelo.jpg} & \includegraphics[scale=0.2]{diagrama-classes.jpg}
\end{tabular}
\end{center}
}

\section{Regras}
\begin{frame}[fragile]
\frametitle{Regras - Regra 1}


Vamos mostrar, para cada regra a que cada esta\c{c}\~ao deve obedecer a sua implementa\c{c}\~ao em Java ou JML

\begin{description}
        \item[Em Alloy] Cada segmento s\'o pode ter no m\'aximo um sem\'aforo.
            \begin{verbatim}
	sema in Track lone -> Semaphore
\end{verbatim}
        \item[Em Java] A vari\'avel de inst\^ancia da classe Seg obedece a essa regra.
\begin{verbatim}
	public Semaphore sema;
\end{verbatim}
       \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 2}
\begin{description}
       \item[Em Alloy] Devem existir sem\'aforos em todos os cruzamentos.
\begin{verbatim}
	all t : Seg | t in overlaps.Seg => one t.sema
\end{verbatim}
\item[Em Java] Foi adicionado o seguinte invariante na classe Track
\begin{verbatim}
	//@ invariant (\forall int i; i >= 0 && 
	 i < overlaps.size(); 
          ((Track) overlaps.get(i)).sema != null);
\end{verbatim}

       \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 3}
\begin{description}
       \item[Em Alloy] Cada segmento s\'o pode ser o seguinte de um segmento.
        \begin{verbatim}
	nexT & (Track -> Track) in Track lone-> Track
\end{verbatim}
\item[Em Java] Na classe Seg, criou-se uma vari\'avel de classe do tipo array de inteiros (nexts) de tamanho n que cont\'em os identificadores de todos os segementos que s\~ao os seguintes de algum segmento. Depois em todos os construtores, quando se especifica o segmento seguinte (n\_next) adiciona-se a pr\'e-condi\c{c}\~ao que indica que o n\_next nao pode j\'a ser seguinte de outro segmento.
        \begin{verbatim}
	//invariante da classe Seg
	//@ invariant n == nexts.length && nexts != null;
	//pre condicao de todos os construtores 
	//da classe Seg
	//@ requires (\forall int i; i >= 0 && 
	i < nexts.length ; nexts[i] != n_next.id);
	//@ requires n < nexts.length;
        \end{verbatim}
        
        \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 4}
\begin{description}
      \item[Em Alloy] Cada segmento n\~ao pode ser o seguinte de si pr\'oprio nem estar sobreposto a si mesmo.
        \begin{verbatim}
	all t:Seg | t not in t.nexT &&
	   t not in t.overlaps
        \end{verbatim}
        \item[Em Java] Na classe Seg e na classe Track respectivamente adicionaram-se os seguintes invariantes.
        \begin{verbatim}
	//@ invariant this != this.next;
	//@ invariant !overlaps.contains(this);
        \end{verbatim}
      \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 5}
\begin{description}
       \item[Em Alloy] Um segmento n\~ao pode ser seguinte e sobreposto de um outro segmento.
        \begin{verbatim}
	all t1,t2:Seg | t1->t2 in nexT =>
	  t1->t2 not in overlaps
        \end{verbatim}
        \item[Java] Na classe Track foi adicionado o seguinte invariante:
        \begin{verbatim}
	//@ invariant this.next != null ==> 
	  !overlaps.contains(this.next);
        \end{verbatim}
        \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 6}
\begin{description}
       \item[Em Alloy] Se o segmento A est\'a sobreposto ao segmento B, ent\~ao o segmento B est\'a sobreposto ao segmento A.
        \begin{verbatim}
    	all t1,t2:Seg | t1->t2 in overlaps =>
	  t2->t1 in overlaps
        \end{verbatim}
        \item[Em Java] Na classe Track foi adicionado o seguinte invariante:
        \begin{verbatim}
	//@ invariant (\forall int i; i>=0 && 
	 i < overlaps.size();
	 (Track) overlaps.get(i)).overlaps.contains(this);
        \end{verbatim}
        \end{description}
\end{frame}

\begin{frame}[fragile]
\frametitle{Regra 7}
\begin{description}
       \item[Em Alloy] Todas as agulhas de sa\'ida (PointOut) t\^em um sem\'aforo.
    	\begin{verbatim}
       	all p_out : PointOut | p_out in Seg => 
     	one p_out.sema
        \end{verbatim}
        \item[Em Java] Na classe PointOut colocou-se o seguinte invariante:
        \begin{verbatim}
      	//@ invariant this.sema != null;
        \end{verbatim}
        \end{description}
\end{frame}

\section{Invariantes de Seguran\c{c}a}

\begin{frame}[fragile]
\frametitle{Invariante de Seguran\c{c}a 1/2}
Para cada Invariante de Seguran\c{c}a foi definida uma especifica\c{c}\~ao JML na classe State.

Invariante : Num segmento n\~ao se encontra mais que um comboio.
\begin{itemize}
\item Alloy
\begin{verbatim}
pred one_train[s:State]{
    all t:Track | lone t.~(s.trains)
}
\end{verbatim}
\item Java
\begin{verbatim}
invariant trains.keySet().size() == 
                trains.entrySet().size();
\end{verbatim}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Invariante de Seguran\c{c}a 2/2}
Invariante : Estando o comboio C no segmento S, n\~ao podem existir comboios nos segmentos sobrepostos a S.
\begin{itemize}
\item Alloy
\begin{verbatim}
pred train_overlap[s:State] {
    all t1,t2 : Train | t1 + t2 in (s.trains).Track =>
           t2.(s.trains) not in (t1.(s.trains)).overlaps
}
\end{verbatim}
\item Java
\begin{verbatim}
invariant (\forall int i;i>=0 && i< trains.size(); 
trains.values().toArray()[i] instanceof Track &&
    (\forall int j;j>=0 && j < ((Track) trains.values().
        .toArray()[i]).overlaps.size();
        !trains.containsValue(((Track)trains.values()
            .toArray()[i]).overlaps.get(j))));
\end{verbatim}
\end{itemize}
\end{frame}


\begin{frame}[fragile]
\frametitle{Opera\c{c}\~oes}
As opera\c{c}\~oes em Alloy foram transformadas em m\'etodos da classe State. Podemos ver agora um peda\c{c}o da opera\c{c}\~ao move em Alloy e respectiva parte no m\'etodo move().

\begin{description}
       \item[Em Alloy]
    	\begin{verbatim}(...)else
	(    (  not (   one (track.nexT).sema &&
	 (track.nexT).sema in s.reds) ) && 
	 (s.trains).(track.nexT) = none ) =>
	  ( move_Train[s,s',t] ) (...)
        \end{verbatim}
        \item[Em Java]
        \begin{verbatim}(...) else {
	 if ((track instanceof Track)) {
	  Track trk = (Track) track;
	  if (!(trk.sema != null && this.reds != null && 
	   this.reds.contains(trk.next.sema)) && 
	   (!this.trains.containsValue(trk.next))){ 
	    this.moveTrain(t);
	    }else {throw new CantMoveException();}}(...)
        \end{verbatim}
        \end{description}
\end{frame}


\begin{frame}[fragile]
\frametitle{Testes usando JUnit}
A realiza\c{c}\~ao de testes permitiu que fossem descobertos erros de constru\c{c}\~ao. Um exemplo desses testes, usando a biblioteca JUnit, verifica se um comboio entra na esta\c{c}\~ao:
\begin{verbatim} (...)
	t4 = new Track();
	tr1 = new Train();
	assertEquals(0, estado.trains.size());
	try {
	estado.move(tr1, (Seg) t4);
	} catch (CantMoveException e) {
	 System.out.println("Cant Move");
	}
	assertEquals(1, estado.trains.size()); (...)
\end{verbatim}
Se este teste n\~ao falhar, \'e sinal que o comboio tr1 entrou na esta\c{c}\~ao e se encontra no segmento t4, ou seja, move adicionou ao HashMap trains a associa\c{c}\~ao entre comboio tr1 e segmento t4. 
\end{frame}

\frame{
\frametitle{Dificuldades do Projecto}

\begin{itemize}
 \item Utiliza\c{c}\~ao do Java 1.4 (a fraca tipagem complica bastante o JML);
 \item O JML (n\~ao est\'a desenvolvido o suficiente);
 \item As ferramentas (apesar do ESC/Java2 ajudar em certos erros, n\~ao \'e fi\'avel para a complexidade deste projecto).
 \item Não conseguimos testar as anota\c{c}\~oes JML
\end{itemize}


}

\frame{
\frametitle{Conclus\~oes do Projecto}
\begin{itemize}
 \item Conseguimos com sucesso recriar o modelo em Java;
 \item Conseguimos especificar atrav\'es do JML, invariantes que inferem seguran\c{c}a \`a esta\c{c}\~ao;
 \item Realizamos testes atrav\'es da framework JUnit, o que se revelou \'util.
\end{itemize}

}

\end{document}